Preliminary User'Manual                                March 26, 1973


Frequently the user of a theorem prover "knows" a lot of detail about

the  problem  domain  being axiomatized.   Much  of  this information

(almost by definiton) is  domain-dependent and  thus doesn't  fit the

usual set  of strategies as  well as could  be desired. Also  much of

this information is  heuristic in nature   and would be  difficlut to

express in the form of  axioms.  To help with these problems  we have

introduced two new ideas:  (1) a language for  describing strategies;

and (2) new data types have  been added to LISP so that the  user may

taylor-make his own prover.

The strategy language  allows Boolean expressions over  properties of

clauses.  Major extensions of this idea are contemplated..

The  programmable aspects  allow the  user to  describe   first order

statements, strategies and pattern matching in an intuitive notation.

With these facilities inside LISP we can write new rules of inference

and domain dependent theorem provers.
Preliminary User'Manual                                March 26, 1973


The Language of Strategies.

(1) Choice strategies.

Choice strategies occur in the following context: Given two  possible

candidates,C1  and  C2,  for  the application  of  a  binary  rule of

inference, I, a choice strategy will determine whether not we wish to

form I(C1,C2).

Builtin choice strategies.

a) NONE  allows unrestricted applications of the rules of inference.

b) ANCESTRY implements the AFF  strategy; that is, to apply  I either

C1 or C2  must be an  initial clauses, or,  either C1 appears  in the

derivation tree of C2, or C2 appears in the tree of C1.

c)  SUPPORT  designates the  set-of-support  strategy.  This strategy

basically says that every first-level deduction must have one  of its

parents in the support set.  SUPPORT must be followed by  an argument

list describing which  statements are to be supported.   The elements

of the argument list may either be clause numbers or names  which the

user has associated with certain input clauses.

Example: SUPPORT[1,2,AXIOM[2],THEOREM]  would put clauses  numbered 1

and 2, the  clause AXIOM[2], and all  clauses with name,  THEOREM, in

the support set.

d) VINE strategy says that either C1 or C2 must be an initial clause.

This strategy is known to be incomplete, but is useful in many cases.

e) UNIT strategy  says that either C1  or C2 are  singletons.  Again,
Preliminary User'Manual                                March 26, 1973


this strategy  is not complete  ,but is useful  as a  "quick-kill" or

"end-game" strategy.   It is easy  to show that  if there is  a UNIT-

refutation then there is a  VINE-form refutation. It is also  easy to

show that if all the initial statements are  either units(singletons)

or are of the form L1∧L2∧...∧Ln ⊃ M then there is a UNIT proof.

f)  P1 is  the P1-deduction  of Robinson.  Here it  is  required that

either  C1 or  C2 contain  only positive  literals. This  strategy is

complete.

g) MODEL is the implementation  of a very simple  case of  the model-

relative deduction strategy of Luckham.  Model-relative  deduction is

a generalization of P1 deduction and is complete.  Deduction relative

to a model says that at least one of the clauses C1 or C2 be false of

the  model.   MODEL  expects an  argument  list  describing  a binary

partition of the predicate letters appearing in the  initial clauses.

In the current  restricted implementation this  says either C1  or C2

must have zero intersection with the two members of the partition.

h) DEFMODEL  can be  used to designate  a LISP  function to  define a

model for the current  set of statements.  DEFMODEL expects  a single

argument which is  the name of a  LISP function(of one  argument) and

which implements the defining conditions of a model.

i) EQUALITY signals that the replacement rule, paramodulation,  is to

be  used.   EQUALITY needs  two  arguments: a  predicate  name  to be

interpreted as equality; and  second, a number, called  PDEPTH, which
Preliminary User'Manual                                March 26, 1973


determines how deep  in the nesting  of function symbols  the matcher

will look in attempting to  match terms.  For example, a PDEPTH  of 1

says only examine primary occurences of terms.
Preliminary User'Manual                                March 26, 1973


(2) Editing Strategies.

Editing  strategies  are  applied  to the  resluts  of  the  rules of

inference.   These strategies  are used  to  filter  out some  of the

deductions which a rule of inference has generated.

Builtin editing strategies.

a)  DEMOD  is  a  rule  of  simplification  most  commonly   used  in

conjunction  with  EQUALITY.  DEMOD takes  two  arguments.  The first

describes a list of equality units; the second, a number named DDEPTH

which,like PDEPTH, determines a bound on the matching routines.

b) DEPTH takes a single integer argument interpreted to be a bound on

the depth of  function symbol nesting which  must not be  exceeded if

the deduction is to be retained.

For example, DEPTH[4].

c) LENGTH  also takes an  integer argument and  gives a bound  on the

number of literals which will be allowed in any deduction.

d)  SELDEPTH  takes   function  symbol-number  pairs   as  arguments.

SELDEPTH is  a refinement  of DEPTH  in that  the allowable  depth of

nesting of  each function symbol  is determined by  the corresponding

number.

e) Any  of the  primitive constructs of  the pattern  language: TREE,

LENGTH, DEPTH, or OCR.  For example if OCR[f(e,e)] were to  appear in

an editing strategy then  any clauses which contained  "f(e,e)" would

be rejected.
Preliminary User'Manual                                March 26, 1973


Boolean  combinations  of  built-in  or  user-defined  strategies are

allowed.   For example,  a reasonable  choice strategy   is: ancestry

filter form with a set of support being the negation of the statement

to be proved.  This can be written as:

 ANCESTRY ∧ SUPPORT[THEOREM];

An editing strategy which filters out all clauses whose length(number

of literals) is  greater than 4 or  whose depth( depth of  nesting of

function symbols) is greater than 3 can be expressed as:

LENGTH[4] ∨ DEPTH [3];

3)  The Automatic Strategy Selection.

A very simple  procedure is used to  select the strategies  in PROVE-

mode.   The choice  strategies are  ANCESTRY and,  if  THEOREMNAME is

present as  an axiom  name ,then  SUPPORT[<value of  THEOREMNAME>] is

also used.  Also, if  an equality predicate letter is  declared, then

equality replacement witha  depth bound of 4 is added.

The  editing strategies  are determined  by the  maximum  lengths and

depths which occur in the input clauses.  If equality is present then

a simplification list consisting of all the positive units is used.

The strategy  settings are  automatically changed  if the  program is

terminated without finding a proof.
Preliminary User'Manual                                March 26, 1973


A programmable theorem prover.

It  is now  possible to  write LISP-like  programs which  control the

actions of  the theroem  prover and  manipulate clauses.   Data types

for CLAUSES, STRATEGIES, and PATTERNS have been added to LISP so that

the user can describe  his clause manipulations in the  same notation

which is used  to drive the  on-line prover.  LISP  functions, TRYTIL

and FIND, have been defined to perform controlled  proof-attempts and

clause-list searching.

1. Data Types.

a) [CLAUSES <clauses>] is used  to introduce new clause lists  to the

program.  For example: (SETQ X [CLAUSES DSK:FOO])  when executed will

assign to X the  clauselist manufactured from the statements  on file

FOO.

b)   [CHOICE  <strategy>]   and  [EDIT   <strategy>]   introduce  the

appropriate strategies.

c) [PATTERN <pattern>] is  useful in conjunction with FIND  to filter

out  clauses which match <pattern>.

2. Procedures.

(TRYTIL         <clauses><choice-strategy><edit-strategy><termination

condition>)

where: 1) <clauses> is a list of clauses . 2) <choice-strategy>  is a

representation of a  choice strategy.  3)  <edit-strategy> represents

an  editing strategy.   4)  <termination condition>  is  a functional
Preliminary User'Manual                                March 26, 1973


argument which will be evaluated periodically during the execution of

the TRYTIL.   As long  as the  condition evaluated  to NIL  the proof

attempt will continue. If the condition becomes true then TRYTIL will

return the list of all deductions which have been made.

For example:

(TRYTIL [CLAUSES  DSK: FOO] [CHOICE  ANCESTRY∧SUPPORT[THEOREM]] [EDIT

LENGTH[4]∨DEPTH[3]] (FUNCTION (LAMBDA()(GREATERP LEVEL 3))) )

will begin  a proof  search using file  DSK:FOO with  choice strategy

being AFF  and supporting  the negation  of the  theorem.  Deductions

whose length is greater than  4 or whose depth of fuction  nesting is

greater than 3 will be discarded.  The proof search will terminate at

the end of level 3.

If a refutation is discovered during any attempt, (QED)  is returned.

If no retutation is found, then the on-line editor is called  to give

the user a chance to examine the current proof environment.  There is

a third  way to exit  TRYTIL: since the  on-line editor  is available

inside the  proof attempt,  typing ABandon  <clauses> to  the  editor

will  force termination  of  the proof  attempt and  will  return the

selected <clauses>.

(FIND <clauses><pattern>)

where:  1)  <clauses>  is  a list  of  clauses.   2)  <pattern>  is a

condition which is to be applied to each element of <clauses>.

The  value of  FIND is  a  list of  all elements  of  <clauses> which

satisfy the <pattern>.
Preliminary User'Manual                                March 26, 1973


THE SYNTAX EQUATIONS FOR THE THEOREM PROVER.

The parsers for  the input syntax and  the command language  are both

contstructed by Lynn Quam's Syntax Directed Input Output program.
Preliminary User'Manual                                March 26, 1973


THE SIMPLE STRATEGY LANGUAGE

The most straightforwrd application of the strategy language consists

of using Boolean combinations of the builtin strategies.

<STRATEGY>::=<F1>;

<F1>    ::=<F2>
        ::=<F1><OR><F2>

<F2>    ::=<F3>
        ::=<F2><AND><F3>

<F3>    ::=(<F1>)
        ::=<NOT><F3>
        ::=<PREDIC>

<PREDIC>::=ANCESTRY
        ::=NONE
        ::=VINE
        ::=UNIT
        ::=P1
        ::=SUPPORT[<C>]
        ::=MODEL[<PREDLST>;<PREDLST>]
        ::=EQUALITY[<OP>,<NUMBER>]
        ::=DEMOD[<CLAUSES>,<NUMBER>]
        ::=DEFMODEL[ID]
        ::=LENGTH[<NUMBER>]
        ::=DEPTH[<NUMBER>]
        ::=SELDEPTH[<FNLST>]
        ::=<MPRM>

<PREDLST>
        ::=<ID>,<PREDLST>
        ::=<ID>
        ::=

<FNLST> ::= <FP>;<FNLST>
        ::= <FP>

<FP>    ::=<OP>,<NUMBER>
Preliminary User'Manual                                March 26, 1973


THE INPUT FORMAT

The usual  form for input  consists of the  declarations of  the non-

logical  constituents  of  the  axioms,  followed  by  a  sequence of

statements.  The statements may be assigned names, and if a statement

whose name is the same as the current value of THEOREMNAME is present

that statement  is negated before  being added to  the memory  of the

prover.
<INPUT> ::=<DECOP>:<OPLIST>;
        ::=<ID>:
        ::=<S>

<DECOP> ::=VAR | INF_OP | INF_PRED | PRE_OP | PRE_PRED | EQUALITY

<OPLIST>::=<OP>,<OPLIST>
        ::=<OP>

<S>     ::=;
        ::=<S1>;

<S1>    ::=<S2>
        ::=<S1><EQUIV><S2>

<S2>    ::=<S3>
        ::=<S2><IMP><S3>

<S3>    ::=<S4>
        ::=<S3><OR><S4>

<S4>    ::=<S5>
        ::=<S4><AND><S5>

<S5>    ::=(<S1>)
        ::=<NOT><S5>
        ::=<QFF><BODY>
        ::=<PRED>

<BODY>  ::= <IVAR><S5>
        ::=(<VARLIST>)<S5>

<VARLIST>::=<IVAR>,<VARLIST>
        ::=<IVAR>
Preliminary User'Manual                                March 26, 1973


In   the  following,the   routines  corresponding   to  <PREPREDLET>,

<INFPREDLET>, <IVAR>, <PREFN>, and <INFN> check the lists  of prefix-

and infix- predicate and function letters, and the variable list, all

of which were manufactured by the appropriate declarations.

<PRED>  ::=<PREPREDLET><ITMLST>
        ::=<TM><INFPREDLET><TM>

<ITMLST>::=(<ITMS>)

<ITMS>  ::=<TM><ITMS>
        ::=<TM>

<TM>    ::=<IVAR>
        ::=<PREFN><ITMLST>
        ::=<PREFN>
        ::=(<TM>)
        ::=<TM><INFN><TM>


The logical connectives are defined as follows:

<EQUIV> ::= ≡ | ↔ 

<IMP>   ::= ⊃

<OR>    ::= ∨

<AND>   ::= ∧

<NOT>   ::= ¬

<QFF>   ::= ∀ | ∃
Preliminary User'Manual                                March 26, 1973



THE COMMAND LANGUAGE


<CLAUSES> ::= <C>,<CLAUSES>
        ::= <C>

<C>     ::= @<S>
        ::= DSK: <FILE>
        ::= <NUMBER>
        ::= <ID>[<VARLIST>]
        ::= <ID>
        ::= FIND [<ID>,<MATCH>]
        ::= FINDC [<MATCH>]

<FILE>  ::= <ID>
        ::= (<ID>.<ID>)

<VARLIST> ::= <NUMBER>,<VARLIST>
        ::= <NUMBER>

<COMMAND ::= AB <CLAUSES>;
        ::= AB;
        ::= AN <CLAUSES>;

        ::= CH;
        ::= CL <ID>;
        ::= CU;

        ::= DE <CLAUSES>;
        ::= DI <CLAUSES>;
        ::= DO <NUMBER>;
        ::= DS <FILE>;

        ::= EO;
        ::= EV;
        ::= EX;

        ::= FD;
        ::= FU;

        ::= GO <NUMBER>;
        ::= HA;
        ::= HE;

        ::= IN <ID> <CLAUSES>;

        ::= ME <CLAUSES>;<CLAUSES>;
Preliminary User'Manual                                March 26, 1973



        ::= PA <CLAUSES>;CLAUSES>;
        ::= PR <CLAUSES>;

        ::= RE <CLAUSES>;<CLAUSES>;

        ::= SA <CLAUSES>;
        ::= SE <ID> <CLAUSES>;
        ::= SI <CLAUSES>; BY <CLAUSES>;
        ::= SU <TM> FOR <TM> IN <CLAUSES>;
        ::= SY;

        ::= TE <CLAUSES>;
        ::= TE;

        ::= UP <NUMBER>;
Preliminary User'Manual                                March 26, 1973


THE MATCHER

<MATCH> ::= <M2>
        ::=<MATCH> ∨ <M2>

<M2>    ::= <M3>
        ::= <M2> ∧ <M3>

<M3>    ::= (<F1>)
        ::=¬<M3>
        ::=<MPRM>

<MPRM>  ::= <ARG><MOP><ARG1>

        ::= OCR[<PAT>]
        ::=TREE[<CNAME>]

<MOP>   ::= =
        ::= <
        ::= >

<ARG1> ::= <ARG>

<ARG>   ::= LENGTH
        ::=DEPTH
        ::=<NUMBER>

<CNAME> ::= <NUMBER>
        ::= <ID>[<VARLIST>]
        ::= <ID>

<PAT>   ::= <NOT1><PRED>
        ::=<PRED>
        ::=<TM>
        ::=<FNLET>